Record/tuple patterns and new pattern match compiler and coverage checker #430

Kmeakin · 2022-12-12T00:41:27Z

Adds record and tuple patterns.
This required rewriting the pattern match compiler and coverage checker, following the algorithms outlined in Compiling pattern matching to good decision trees and Warnings for pattern matching, respectively
The new algorithms can be extended in the future to support more pattern matching features, such as or-patterns and pattern guards.

Future work

I have not done any optimization: there are a lot of allocations that could probably be eliminated.
The coverage checker simply reports that a match is in-exhaustive, but does not explain which patterns are missing. A more sophisticated algorithm for calculating missing patterns in described in the second half of "Warnings for pattern matching"
The implementation of shift is inefficient: we may want to add a new Weaken term kind instead
The match compiler produces ugly code: it inserts extra let bindings in the body of default branches, instead of binding the default branch to a variable:

match x {
    0 => 0,
    y => y + 1,
}

will become

match x {
    0 => 0,
    _ => let y = x; y + 1,
}

wezm

I'll leave a full review of this to when Brendan returns from leave. Just noting one small issue with links in docs.

fathom/src/surface/elaboration/patterns/compile.rs

brendanzab

Still need to look deeper into this to try to understand the algorithm… there’s a bit to take in but it’s looking neat!

fathom/src/core.rs

fathom/src/surface/elaboration/patterns.rs

fathom/tests/source_tests.rs

fathom/src/surface/elaboration/patterns/compile.rs

fathom/src/core.rs

brendanzab · 2022-12-16T05:32:02Z

We could maybe pull out the rust upgrade into a separate PR if it helps clean things up.

Kmeakin · 2022-12-18T02:18:58Z

We could maybe pull out the rust upgrade into a separate PR if it helps clean things up.

That was the intention, not sure why github included those commits in the PR. Fixed it now.

fathom/src/surface/elaboration.rs

fathom/src/surface.rs

fathom/src/env.rs

fathom/src/core/semantics.rs

tests/fail/elaboration/boolean-literal/not-supported.snap

brendanzab · 2023-01-17T04:50:19Z

fathom/src/surface/distillation.rs

+#[allow(clippy::type_complexity)]
 fn match_if_then_else<'arena>(
    branches: &'arena [(Const, core::Term<'arena>)],
    default_branch: Option<(Option<StringId>, &'arena core::Term<'arena>)>,
-) -> Option<(&'arena core::Term<'arena>, &'arena core::Term<'arena>)> {
+) -> Option<(
+    (Option<Option<StringId>>, &'arena core::Term<'arena>),
+    (Option<Option<StringId>>, &'arena core::Term<'arena>),
+)> {


I’m… not really understanding what’s going on with the Option<Option<StringId>>s for the then and else branches?

In cases of the form

match x { true => ..., _ => ..., }

or

match x { false => ..., _ => ..., }

We have to push _ onto local_names, or else we get confusing bugs in distillation output. Alternatively, we could only distill matches to if-then-else syntax if they are of the form

match x { true => ..., false => ..., }

brendanzab · 2023-01-17T04:51:01Z

Sorry for the slowness - taking a bit of time to get into this one

brendanzab · 2023-01-25T04:34:46Z

I’ve been looking at this more in depth locally. Doing a bit of messing around to understand it a bit more and tweaking the implementation a bit. While it’s big, I think it would be better to squash it into a single commit as it kind of only works all together.

One nit-pick: could we use the actual the actual type names rather than Self in impls and type definitions etc? I prefer to only use those when necessary in trait definitions.

Kmeakin · 2023-01-27T12:45:31Z

One nit-pick: could we use the actual the actual type names rather than Self in impls and type definitions etc? I prefer to only use those when necessary in trait definitions.

I think the preferred Rust style is to use Self wherever possible: https://rust-lang.github.io/rust-clippy/master/#use_self. Personally I prefer Self because:

Usually less typing: most type names are more than 4 letters. Also allows you to avoid repeating lifetimes/type parameters
One less piece of information you need to keep track off when writing methods/impls. Never do something yourself that the compiler can do for you!
Type names may change frequently during development. Self means you don't have to update all the occurrences of the type name, and keeps diffs smaller

brendanzab · 2023-01-31T07:23:17Z

fathom/src/surface/elaboration/patterns.rs

+                let columns =
+                    vec![(CheckedPattern::Placeholder(*range), scrut.clone()); ctor.arity()];


Why is it ok to duplicate these without updating scrut?

A wildcard pattern leaves the scrutinee unchanged: it does not project further into it. It is duplicated ctor.arity() times because the algorithm relies on the matrix always being rectangular.

Oh, was more wondering about the type of the scrutinee - does it need to be updated for each pattern (seeing as it seems like this is based on the arity of the constructor) or is that unecessary?

No, updating the type is also unnecessary. The scrutinee is left completely unchanged by wildcard patterns because wildcard patterns match anything: they don't inspect or transform the scrutinee in any way

brendanzab · 2023-02-06T00:16:48Z

I’ve looked into merging this, trying to do some cleaning up (see: Kmeakin/fathom@pattern-matching...brendanzab:fathom:pattern-matching-cleanups), but I don’t think it is ready yet. Some of the pattern matching compilation is self-contained and can be iterated on for improved clarity, but my big fear is how it impacts the handling of local bindings in the elaborator. The freshen_scrutinee and insert_extra_let methods are of particular concern, and I’m a little worried about taking on this burden going forward. Related to #488, it does make me think we might need a better approach to managing local bindings in the elaborator - eg. regarding adding/removing bindings, or with weakening.

Kmeakin force-pushed the pattern-matching branch 3 times, most recently from 1ef64a4 to d24c4f9 Compare December 12, 2022 01:28

wezm reviewed Dec 13, 2022

View reviewed changes

fathom/src/surface/elaboration/patterns/compile.rs Outdated Show resolved Hide resolved

Kmeakin marked this pull request as draft December 14, 2022 01:35

brendanzab reviewed Dec 16, 2022

View reviewed changes

fathom/src/core.rs Outdated Show resolved Hide resolved

fathom/src/surface/elaboration/patterns.rs Outdated Show resolved Hide resolved

fathom/tests/source_tests.rs Show resolved Hide resolved

fathom/src/surface/elaboration/patterns/compile.rs Outdated Show resolved Hide resolved

brendanzab reviewed Dec 16, 2022

View reviewed changes

fathom/src/core.rs Outdated Show resolved Hide resolved

Kmeakin force-pushed the pattern-matching branch 3 times, most recently from 792176f to c31c1d1 Compare December 20, 2022 13:47

brendanzab reviewed Dec 21, 2022

View reviewed changes

fathom/src/surface/elaboration.rs Outdated Show resolved Hide resolved

Kmeakin force-pushed the pattern-matching branch from c31c1d1 to 9dcfafa Compare December 21, 2022 15:20

Kmeakin marked this pull request as ready for review December 21, 2022 15:22

Kmeakin requested a review from brendanzab December 21, 2022 15:22

Kmeakin force-pushed the pattern-matching branch 2 times, most recently from 7003365 to 86aa0c6 Compare December 21, 2022 16:30

Kmeakin force-pushed the pattern-matching branch 8 times, most recently from 8dbe29a to 25f66bc Compare January 17, 2023 03:09

brendanzab reviewed Jan 17, 2023

View reviewed changes

Kmeakin force-pushed the pattern-matching branch 2 times, most recently from e91303c to cccdfb7 Compare January 17, 2023 06:11

Kmeakin force-pushed the pattern-matching branch 4 times, most recently from e3ff50e to 4cef50e Compare January 23, 2023 14:38

Kmeakin force-pushed the pattern-matching branch from 4cef50e to bc914d7 Compare January 27, 2023 12:33

Kmeakin force-pushed the pattern-matching branch from bc914d7 to 3917860 Compare January 30, 2023 16:28

brendanzab reviewed Jan 31, 2023

View reviewed changes

Kmeakin force-pushed the pattern-matching branch 4 times, most recently from fdd2ba7 to 90af406 Compare February 1, 2023 00:42

Kmeakin force-pushed the pattern-matching branch from 90af406 to 8e82b43 Compare February 7, 2023 01:49

Kmeakin added 2 commits September 3, 2023 22:25

Update broken dependecies

6e2d6a7

Record and tuple patterns, new pattern match compiler

696a03e

Kmeakin force-pushed the pattern-matching branch from 8e82b43 to 696a03e Compare September 5, 2023 11:04

		let columns =
		vec![(CheckedPattern::Placeholder(*range), scrut.clone()); ctor.arity()];

Record/tuple patterns and new pattern match compiler and coverage checker #430

Are you sure you want to change the base?

Record/tuple patterns and new pattern match compiler and coverage checker #430

Uh oh!

Conversation

Kmeakin commented Dec 12, 2022 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Future work

Uh oh!

wezm left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

brendanzab left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

brendanzab commented Dec 16, 2022

Uh oh!

Kmeakin commented Dec 18, 2022

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

brendanzab Jan 17, 2023

Choose a reason for hiding this comment

Uh oh!

Kmeakin Jan 17, 2023

Choose a reason for hiding this comment

Uh oh!

brendanzab commented Jan 17, 2023

Uh oh!

brendanzab commented Jan 25, 2023

Uh oh!

Kmeakin commented Jan 27, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

brendanzab Jan 31, 2023

Choose a reason for hiding this comment

Uh oh!

Kmeakin Feb 1, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

brendanzab Feb 2, 2023

Choose a reason for hiding this comment

Uh oh!

Kmeakin Feb 2, 2023

Choose a reason for hiding this comment

Uh oh!

brendanzab commented Feb 6, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Kmeakin commented Dec 12, 2022 •

edited

Loading

Kmeakin commented Jan 27, 2023 •

edited

Loading

Kmeakin Feb 1, 2023 •

edited

Loading

brendanzab commented Feb 6, 2023 •

edited

Loading